We present the system SUBSEXPL used for simulating and comparing explicit substitutions calculi. The system allows the manipulation of expressions of the λ-calculus and of three different styles of explicit substitutions: the λσ, the λse and the suspension calculus. A variation of the suspension calculus, which allows for combination of steps of β-contraction is included too. Implementations of the η-reduction are provided for each style. Other explicit substitutions calculi can be easily incorporated into the system due to its modular structure. (...) The uses of the system include: the visualization of the contractions of the λ-calculus in de Bruijn notation, and of guided one-step reductions as well as normalization via each of the associated substitution calculi. Many useful facilities are included: reductions can be easily recorded as text files, LATEX outputs can be generated and several examples for dealing with arithmetic operations and computational operators such as conditionals and repetitions in the λ-calculus are available. The system can be executed over Emacs using the x-symbol mode in such a way that λ-terms and terms of the explicit substitutions calculi are represented in its natural syntax avoiding the necessity of repeatedly generating LATEX outputs. The system has been of great help for systematically comparing explicit substitutions calculi, as well as for understanding properties of explicit substitutions such as the Preservation of Strong Normalization. In addition, it has been used for teaching basic properties of the λ-calculus such as: computational adequacy, the usefulness of de Bruijn's notation and of making explicit substitutions in real implementations. (shrink)

The past decade has seen an explosion of work on calculi of explicit substitutions. Numerous works have illustrated the usefulness of these calculi for practical notions like the implementation of typed functional programming languages and higher order proof assistants. It has also been shown that eta-reduction is useful for adapting substitution calculi for practical problems like higher order unification. This paper concentrates on rewrite rules for eta-reduction in three different styles of explicit substitution calculi: λσ, λse and the suspension calculus. (...) Both λσ and λse when extended with eta-reduction rules, have proved useful for solving higher order unification. We enlarge the suspension calculus with an adequate eta-reduction rule which we show to preserve termination and confluence of the associated substitution calculus and to correspond to the eta rules of the other two calculi. We prove that λσ and λse as well as λσ and the suspension calculus are non-comparable while λse is more adequate than the suspension calculus in simulating one-step beta-reduction. After defining the eta-reduction rule in the suspension calculus, and after comparing these three calculi of explicit substitutions , we then concentrate on the implementation of the rewrite rules of eta-reduction in these calculi. We note that it is usual practice when implementing the eta rule for substitution calculi, to mix isolated applications of eta-reduction with the application of other rules of the corresponding substitution calculi. The main disadvantage of this practice is that the eta rewrite rules so obtained are unclean because they have an operational semantics different from that of the eta-reduction of the λ-calculus. For the three calculi in question enlarged with adequate eta rules we show how to implement these eta rules. For the λse we build a clean implementation of the eta rule and we prove that it is not possible to follow the same approach for the λσ and λsusp. (shrink)

This article is part of a For-Discussion-Section of Methods of Information in Medicine about the paper "Biomedical Informatics: We Are What We Publish", written by Peter L. Elkin, Steven H. Brown, and Graham Wright. It is introduced by an editorial. This article contains the combined commentaries invited to independently comment on the Elkin et al. paper. In subsequent issues the discussion can continue through letters to the editor.

Our goal was to explore self‐care practices among men who have sex with men in the context of Mpox in Brazil. This study used qualitative research methods, including interviews and thematic analysis, to collect and analyze data from male participants across the Brazilian territory. The narratives unveil men's perspectives on self‐care, risk reduction, and health beliefs during the Mpox pandemic. Our findings highlight a multifaceted approach to self‐care among men, encompassing hygiene, physical contact management, mask usage, skin lesion vigilance, and (...) adherence to official guidelines. Men's attitudes toward sexual behaviors emphasize the importance of reducing sexual partners, practicing safe sex, and combating misinformation through accurate information dissemination. The development of these behaviors and self‐care practices can be facilitated by nurses guided by Dorothea Orem's Self‐Care Theory, supported by patient‐centered care, with strategies to address and confront the stigma associated with the disease and provide emotional support. Thus, the study underscores the pivotal role of self‐care in mitigating infection risks, especially in the context of emerging infectious diseases. It acknowledges the impact of socio‐cultural factors and healthcare policies on men's preventive measures. However, it also recognizes limitations, such as potential bias due to stigma concerns and a nonrepresentative sample. Ultimately, the research advocates for tailored education, promotion of gender equity, and healthcare empowerment to effectively manage health risks in such contexts. (shrink)

The US neutrino community gathered at the Workshop on the Intermediate Neutrino Program at Brookhaven National Laboratory February 4-6, 2015 to explore opportunities in neutrino physics over the next five to ten years. Scientists from particle, astroparticle and nuclear physics participated in the workshop. The workshop examined promising opportunities for neutrino physics in the intermediate term, including possible new small to mid-scale experiments, US contributions to large experiments, upgrades to existing experiments, R&D plans and theory. The workshop was organized into (...) two sets of parallel working group sessions, divided by physics topics and technology. Physics working groups covered topics on Sterile Neutrinos, Neutrino Mixing, Neutrino Interactions, Neutrino Properties and Astrophysical Neutrinos. Technology sessions were organized into Theory, Short-Baseline Accelerator Neutrinos, Reactor Neutrinos, Detector R&D and Source, Cyclotron and Meson Decay at Rest sessions.This report summarizes discussion and conclusions from the workshop. (shrink)

Current UK legislation is impacting upon the feasibility and cost-effectiveness of medical record-based research aimed at benefiting the NHS and the public heath. Whereas previous commentators have focused on the Data Protection Act 1998, the Health and Social Care Act 2001 is the key legislation for public health researchers wishing to access medical records without written consent. The Act requires researchers to apply to the Patient Information Advisory Group for permission to access medical records without written permission. We present a (...) case study of the work required to obtain the necessary permissions from PIAG in order to conduct a large scale public health research project. In our experience it took eight months to receive permission to access basic identifying information on individuals registered at general practices, and a decision on whether we could access clinical information in medical records without consent took 18 months. Such delays pose near insurmountable difficulties to grant funded research, and in our case £560 000 of public and charitable money was spent on research staff while a large part of their work was prohibited until the third year of a three year grant. We conclude by arguing that many of the current problems could be avoided by returning PIAG’s responsibilities to research ethics committees, and by allowing “opt-out” consent for many public health research projects. (shrink)

Le présent article part d’une proposition de Giorgio Agamben issue du livre La communauté qui vient, consistant à penser une communauté non appropriable, c’est-à-dire, une communauté pour des individus ontologiquement indéterminés et qui ne pouvant pas être appropriés par les appareils du pouvoir. En ce sens, nous essayons de montrer comment la formation sociale conçue par Agamben peut dialoguer avec l’idée de multitude de Michael Hardt et Antonio Negri. À cette fin, sont exposées les similitudes entre la communauté « qui (...) vient » de Agamben et la multitude. En séquence, nous discutons le rôle individualisant de la loi et de la politique occidentale, comprises comme mécanismes hiérarchiques dont la fonction est précisément d’empêcher l’émergence de la multitude. (shrink)

Le présent article part d’une proposition de Giorgio Agamben issue du livre La communauté qui vient, consistant à penser une communauté non appropriable, c’est-à-dire, une communauté pour des individus ontologiquement indéterminés et qui ne pouvant pas être appropriés par les appareils du pouvoir. En ce sens, nous essayons de montrer comment la formation sociale conçue par Agamben peut dialoguer avec l’idée de multitude de Michael Hardt et Antonio Negri. À cette fin, sont exposées les similitudes entre la communauté « qui (...) vient » de Agamben et la multitude. En séquence, nous discutons le rôle individualisant de la loi et de la politique occidentale, comprises comme mécanismes hiérarchiques dont la fonction est précisément d’empêcher l’émergence de la multitude. (shrink)

We present the idea of searching for X-rays as a signature of the mechanism inducing the spontaneous collapse of the wave function. Such a signal is predicted by the continuous spontaneous localization theories, which are solving the “measurement problem” by modifying the Schrödinger equation. We will show some encouraging preliminary results and discuss future plans and strategy.

Dans cet article nous avons essayé d'examiner la valeur de l'attribution traditionelle du commentaire De Anima à Simplicius. En comparant ce traité aux grands commentaires de Simplicius (sur les Catégories, la Physique et le De Caelo d'Aristote), nous avons été en effet frappés par les divergences de style, et de langue, ainsi que par la différente manière de commenter. Dans la première partie nous démontrons que l'auteur de l'In D.A. a écrit également la Metaphrasis in Theophrastum, qui nous a été (...) transmise sous le nom de Priscien le Lydien. 1° Dans le In D.A. l'auteur renvoie à une de ses œuvres, qu'il appelle „Epitomé de la Physique de Théophraste". En réalité, cette référence se rapporte à un passage de la Métaphrase de Priscien, où la même problématique est exposée dans des termes identiques. — 2° Une comparaison détaillée, qui porte sur l'ensemble des deux œuvres, nous révèle une telle ressemblance de style et de pensée — il y a même des phrases à peu près identiques — qu'elle ne peut s'expliquer que par l'hypothèse de l'identité de l'auteur. Dans la deuxième partie nous essayons d'identifier l'auteur de ces deux œuvres qui pourtant nous ont été transmises sous deux noms différents. L'étude de la tradition directe et indirecte n'apporte guère de solution, puisque l'attribution des deux textes, l'un à Simplicius, l'autre à Priscien, y paraît très solide. Ce n'est donc que par une critique interne de l'In D.A., notamment par la confrontation avec les commentaires de Simplicius, dont l'attribution est certaine, que la question pourra être tranchée. 1° Dans l'In D.A. l'auteur renvoie trois fois à son commentaire sur la Physique. Pourtant, il est bien difficile de retrouver dans le grand commentaire de Simplicius trois passages dont le contenu et surtout le vocabulaire prouvent que l'auteur s'y réfère. — 2° Dans l'In D.A. on ne retrouve pas les traits caractéristiques de la méthode de commenter de Simplicius, ni l'approche du texte par la documentation historique, ni les longues discussions avec les exégètes antérieurs, ni l'exposé prolixe et bien structuré; d'autre part aucun des commentaires de Simplicius ne témoigne de la phraséologie tortueuse de notre oeuvre, ni de ses formules stéréotypées. — 3° La différence doctrinale est encore plus importante. Nulle part chez Simplicius n'apparaît la théorie de l'âme comme όριστική, qui est si fondamentale dans l'In D.A. (όρίζω y est un concept-clé). Les rares digressions de l'In D.A. à propos de questions physiques et logiques ne correspondent pas aux exposés de Simplicius sur les mêmes problèmes. Ainsi nous avons confronté la doctrine de la ‚physis', de l'âme et de son ‚automotion’ et enfin le rapport entre le ‚genre’ et les différences ‚constitutives’ et ‚diérétiques’. De tout cela se dégage une telle divergence entre l'In D. A. et les autres commentaires qu'elle ne peut s'expliquer par une évolution chez Simplicius lui-même. L'in D.A. lui est donc faussement attribué; et puisque nous avons établi que ce commentaire est du même auteur que la Métaphrase, nous pouvons conclure qu'il a été vraisemblablement écrit par Priscien le Lydien, un philosophe néoplatonicien dont nous savons seulement qu'il a accompagné Damascius et Simplicius en exil en Perse. (shrink)

Here are the 18 guidance points contained in the UNAIDS document on Ethical Considerations in HIV Preventive Vaccine Research, reproduced by kind permission of the Joint United Nations Programme on HIV/AIDS.